da1,da2:fpf(Knd; x.Type).
normal-da{i:l}(da1)  normal-da{i:l}(da2)  normal-da{i:l}(fpf-join(Kind-deq; da1; da2)) 

latex

Definitions	False, P  Q, A, left + right, P  Q, b, x:A. B(x), t  T, b, , s = t, prop{i:l}, Knd, Type, x.A(x), x. t(x), fpf(A; a.B(a)), top, x:AB(x), Kind-deq, fpf-dom(eq; x; f), x:A  B(x), P  Q, P  Q, Unit, void, isect(A; x.B(x)), fpf-join(eq; f; g), fpf-ap(f; eq; x), normal-type{i:l}(T), fpf-all(A; eq; f; x,v.P(x;v)), normal-da{i:l}(da)
Lemmas	normal-da wf, fpf wf, fpf-join wf, top wf, fpf-join-ap-sq, fpf-join-dom, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf